#include "UnaryClausesRemover.cuh"
#include "../FileManager/Lex_byacc/cnf_reader.cuh"

UnaryClausesRemover::UnaryClausesRemover(vector<Clause> * formula_host, int number_of_vars)
{
	this->formula_host = formula_host;
	this->status = UNDEF;
	this->number_of_variables = number_of_vars;
}

void UnaryClausesRemover::process_unary_clauses()
{
	for(std::vector<Clause>::iterator it = formula_host->begin();
			it != formula_host->end(); ++it)
	{
		Clause c = *it;

		if(c.number_of_lits == 1)
		{
			Lit lit = c.literals[0];

			if(add(lit))
			{
				formula_host->erase(it);
				it--;
			}

		}

	}
/*
	if(set_literals.size() == number_of_variables)
	{
		status = SAT;
	}
*/
}

bool UnaryClausesRemover::add(Lit literal)
{

	for(std::vector<Lit>::iterator it2 = set_literals.begin();
			it2 != set_literals.end(); ++it2)
	{
		if(literal == *it2)
		{
			return false;
		}
		if((~literal) == *it2)
		{
			status = UNSAT;
			return false;
		}

	}

	set_literals.push_back(literal);
	return true;

}

sat_status UnaryClausesRemover::process_clause(std::vector<Lit> & implied_lits,
		Clause c, Lit & unit_lit)
{
	Lit l1, l2;

	l1 = mkLit(204, false);
	l2 = mkLit(110, true);

	int unsat_lits = 0;

	for(int i = 0; i < c.number_of_lits; i++)
	{
		Lit clause_current = c.literals[i];
		bool current_unsat = false;

		for(std::vector<Lit>::iterator it = implied_lits.begin(); it < implied_lits.end(); it++)
		{
			Lit implied_current = *it;

			if(clause_current == implied_current)
			{
				unit_lit.x = -1;
				return SAT;
			}

			if(clause_current == ~implied_current)
			{
				unsat_lits++;
				current_unsat = true;
				break;
			}
		}

		if(!current_unsat)
		{
			unit_lit = clause_current;
		}

	}

#ifdef USE_ASSERTIONS
	assert(unsat_lits >= 0 && unsat_lits <= c.number_of_lits);
#endif

	if(unsat_lits != c.number_of_lits - 1)
	{
		unit_lit.x = -1;
	}

	return unsat_lits == c.number_of_lits ? UNSAT : UNDEF;

}

void UnaryClausesRemover::clean_clause(std::vector<Lit> & implied_lits, Clause & c)
{
	for(int i = 0; i < c.number_of_lits; i++)
	{
		Lit clause_current = c.literals[i];
		for(std::vector<Lit>::iterator it = implied_lits.begin(); it < implied_lits.end(); it++)
		{
			Lit implied_current = *it;
#ifdef USE_ASSERTIONS
			assert(!(clause_current == implied_current));
#endif
			if(clause_current == ~implied_current)
			{
				remove_literal(c, i);
				i--;
			}

		}
	}
}

void UnaryClausesRemover::propagate_literals()
{
	std::vector<Clause>::iterator it = formula_host->begin();

	while(it != formula_host->end())
	{
		Clause c = *it;
		Lit learnt;

		sat_status stat = process_clause(set_literals, c, learnt);

		if(learnt.x != -1)
		{
			add(learnt);
			if(status == UNSAT)
			{
				return;
			}
		}

		if(stat == SAT || learnt.x != -1)
		{
			formula_host->erase(it);
		}
		else
		{
			if(stat == UNSAT)
			{
				status = UNSAT;
				return;
			}
			else
			{
				clean_clause(set_literals, *it);
				it++;
			}
		}

	}

	if(formula_host->size() == 0)
		status = SAT;

}



void UnaryClausesRemover::process()
{
	process_unary_clauses();

	if(status != UNDEF)
		return;

	int last_num_lit = 0;
	int current_num_lit = set_literals.size();

	while(current_num_lit != last_num_lit)
	{
		propagate_literals();
		if(status != UNDEF)
			return;

		last_num_lit = current_num_lit;
		current_num_lit = set_literals.size();

	}

#ifdef USE_ASSERTIONS
	assert(test_results());
#endif


}

sat_status UnaryClausesRemover::get_status()
{
	return status;
}

bool UnaryClausesRemover::test_results()
{
	if(status != UNDEF)
		return true;

	for(std::vector<Clause>::iterator it = formula_host->begin();
			it != formula_host->end(); ++it)
	{
		if((*it).number_of_lits <= 1)
		{
			printf("Empty or unary clause stored!\n");
			return false;
		}
		for(std::vector<Lit>::iterator it2 = set_literals.begin();
				it2 != set_literals.end(); ++it2)
		{
			for(int i = 0; i < (*it).number_of_lits; i++)
			{
				if(var(*it2) == var((*it).literals[i]))
				{
					printf("The clause ");
					print_clause((*it));
					printf(" that contains the removed literal ");
					print_lit(*it2);
					printf(" remains in the formula!\n");
					return false;
				}
			}
		}
	}
	return true;
}

void UnaryClausesRemover::print_set_literals()
{
	printf("Set literals = [ ");
	for(std::vector<Lit>::iterator it = set_literals.begin(); it != set_literals.end(); ++it)
	{
		print_lit(*it);
		printf(" ");
	}
	printf("]\n");
}

void UnaryClausesRemover::print_host_formula()
{
	printf("Formula:\n");
	for(std::vector<Clause>::iterator it = formula_host->begin(); it != formula_host->end(); ++it)
	{
		print_clause((*it));
		printf("\n");
	}
}

void UnaryClausesRemover::get_set_literals(vector< Lit > & literals)
{
	literals.insert(literals.end(), set_literals.begin(), set_literals.end());
}
